Emit a compile-time warning when a function with #[kani::recursion] is involved in mutual recursion. The per-function REENTRY mechanism only handles direct recursion soundly and mutual recursion silently produces unsound results with no diagnostic.

Contributes to #3316, #3273.

Problem

The #[kani::recursion] attribute uses a per-function REENTRY flag to detect when a function calls itself, replacing the recursive call with the function's contract. For mutual recursion (f calls g, g calls f), the REENTRY flag for g is never set when verifying f's contract, so g's body executes fully instead of being replaced by its contract. This is a silent soundness gap — verification succeeds but the result is meaningless.

Solution

• check_mutual_recursion() in contracts.rs: When a function with #[kani::recursion] is being processed in RecursiveCheck mode, scans its MIR body for calls to other functions that have contracts. For each such callee, checks if the callee's body calls back to the original function (one level of indirection). If so, emits a span_warn at the call site.
• Only one warning per function to avoid noise.
• Only checks one level of indirection (f→g→f). Deeper chains (f→g→h→f) are not detected — this is a known limitation documented in the warning.

Example warning

warning: `#[kani::recursion]` is used on `mutual_a`, which calls `mutual_b`
         that calls back to `mutual_a`. Mutual recursion is not supported by
         contract verification and may produce unsound results. Only direct
         recursion (a function calling itself) is handled correctly.
  --> tests/expected/function-contract/mutual_recursion_unsound.rs:12:30

Testing

• mutual_recursion_unsound.rs — two mutually recursive functions (mutual_a ↔ mutual_b) with contracts and #[kani::recursion], verifying the warning is emitted.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.